1. Technical Field
The present invention relates in general to verifying designs and in particular to performing reduction of subexpressions. Still more particularly, the present invention relates to a system, method and computer program product for performing reduction of subexpressions in structural design representations containing AND and OR gates.
2. Description of the Related Art
With the increasing penetration of processor-based systems into every facet of human activity, demands have increased on the processor and application-specific integrated circuit (ASIC) development and production community to produce systems that are free from design flaws. Circuit products, including microprocessors, digital signal and other special-purpose processors, and ASICs, have become involved in the performance of a vast array of critical functions, and the involvement of microprocessors in the important tasks of daily life has heightened the expectation of error-free and flaw-free design. Whether the impact of errors in design would be measured in human lives or in mere dollars and cents, consumers of circuit products have lost tolerance for results polluted by design errors. Consumers will not tolerate, by way of example, miscalculations on the floor of the stock exchange, in the medical devices that support human life, or in the computers that control their automobiles. All of these activities represent areas where the need for reliable circuit results has risen to a mission-critical concern.
In response to the increasing need for reliable, error-free designs, the processor and ASIC design and development community has developed rigorous, if incredibly expensive, methods for testing and verification for demonstrating the correctness of a design. The task of hardware verification has become one of the most important and time-consuming aspects of the design process.
Among the available verification techniques, formal and semiformal verification techniques are powerful tools for the construction of correct logic designs. Formal and semiformal verification techniques offer the opportunity to expose some of the probabilistically uncommon scenarios that may result in a functional design failure, and frequently offer the opportunity to prove that the design is correct (i.e., that no failing scenario exists).
Unfortunately, the resources needed for formal verification, or any verification, of designs are proportional to design size. Formal verification techniques require computational resources which are exponential with respect to the design under test. Simulation scales polynomially and emulators are gated in their capacity by design size and maximum logic depth. Semi-formal verification techniques leverage formal algorithms on larger designs by applying them only in a resource-bounded manner, though at the expense of incomplete verification coverage. Generally, coverage decreases as design size increases.
Techniques for reducing the size of a design representation have become critical in numerous applications. Logic synthesis optimization techniques are employed to attempt to render smaller designs to enhance chip fabrication processes.
Numerous techniques have been proposed for reducing the size of a structural design representation. For example, redundancy removal techniques attempt to identify gates in the design which have the same function, and merge one onto the other. Such techniques tend to rely upon binary decision diagram (BDD)-based or satisfiability (SAT)-based analysis to prove redundancy, which tend to be computationally expensive. Another technique is subexpression elimination, wherein a system rewrites logic expressions to attempt to enable a representation with fewer gates. For example, given two expressions A&B&C and D&A&B, subexpression elimination would translate those to (A&B)&C and (A&B)&D, enabling a sharing of node (A&B) between both expressions, requiring a total of three 2-bit AND expressions vs. four. Traditionally, such subexpression elimination algorithms require the use of logic factoring algorithms for obtaining covers of expanded forms of logic expressions, which also tend to be costly in terms of computational resources.
What is needed is a method, system, and computer program product for heuristic subexpression elimination on a structural design representation containing AND and OR gates.